ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A,B:ecl-trans-tuple{i:l}(ds; da),
f:(()()), g:(), L,L1,l:(event-info(ds;da) List).
(L = append(L1; l))
 (L':(event-info(ds;da) List). 
 iseg(event-info(ds;da); L'; L)
  (iseg(event-info(ds;da); L1; L')  ((ecl-trans-h(A)(0,ecl-trans-state(A; L'))))))
 (ecl-trans-state(combine-ecl-tuples(A; B; f; g); L)
 (=
 (<ecl-trans-state(A; L), ecl-trans-state(B; l)>
 ( ecl-trans-type(combine-ecl-tuples(A; B; f; g))) 

latex

Definitions

guard(T), True, T, P  Q, tt, ff, t.2, if b then t else f fi , ma-valtype(da; k), ecl-trans-h(v), ||as||, P  Q, P  Q, P  Q, subtype(S; T), top, Y, list_accum(x,a.f(x;a); y; l), ecl-trans-init(v), ecl-trans-state-from(v; z; L), ecl-trans-state(v; L), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), t.1, False, A, A  B, x. t(x), t  T, prop{i:l}, combine-ecl-tuples(A; B; f; g), ecl-trans-type(A), P  Q, , x:A. B(x), Unit, event-info(ds;da), , x:A. B(x), null(as), b, decidable(P), x(s), ecl-trans-tuple{i:l}(ds; da),

Lemmas

member append, or functionality wrt iff, assert of bor, bnot thru band, true wf, squash wf, bor wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, and functionality wrt iff, assert of band, band wf, assert-deq-member, eqtt to assert, l member wf, iff transitivity, Kind-deq wf, deq-member wf, iseg append0, iseg weakening, cons one one, ecl-trans-state-from wf, ecl-trans-state-append, iseg append, length wf1, append-cancellation, append-cancellation-right, last wf, append assoc, last lemma, iseg antisymmetry, combine-ecl-trans-state0, append nil sq, top wf, null wf3, decidable assert, append is nil, Id wf, Knd wf, fpf wf, ecl-trans-tuple wf, nat wf, bool wf, subtype rel self, combine-ecl-tuples wf, ecl-trans-type wf, ecl-trans-state wf, le wf, ecl-trans-h wf, assert wf, iff wf, iseg wf, append wf, event-info wf, last induction